(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X
Rewrite Strategy: FULL
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(2n):
The rewrite sequence
activate(n__first(n__from(X62970_3), X2)) →+ first(cons(activate(X62970_3), n__from(n__s(activate(X62970_3)))), activate(X2))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0].
The pumping substitution is [X62970_3 / n__first(n__from(X62970_3), X2)].
The result substitution is [ ].
The rewrite sequence
activate(n__first(n__from(X62970_3), X2)) →+ first(cons(activate(X62970_3), n__from(n__s(activate(X62970_3)))), activate(X2))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,1,0,0].
The pumping substitution is [X62970_3 / n__first(n__from(X62970_3), X2)].
The result substitution is [ ].
(2) BOUNDS(2^n, INF)
(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0' → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X
S is empty.
Rewrite Strategy: FULL
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0' → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X
Types:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1
(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
sel,
activate,
sel1,
quote,
first1,
quote1,
unquote,
unquote1They will be analysed ascendingly in the following order:
sel = activate
activate < sel1
activate < quote
activate < first1
activate < quote1
sel1 = quote
quote < first1
quote < quote1
first1 < quote1
unquote < unquote1
(8) Obligation:
TRS:
Rules:
sel(
s(
X),
cons(
Y,
Z)) →
sel(
X,
activate(
Z))
sel(
0',
cons(
X,
Z)) →
Xfirst(
0',
Z) →
nilfirst(
s(
X),
cons(
Y,
Z)) →
cons(
Y,
n__first(
X,
activate(
Z)))
from(
X) →
cons(
X,
n__from(
n__s(
X)))
sel1(
s(
X),
cons(
Y,
Z)) →
sel1(
X,
activate(
Z))
sel1(
0',
cons(
X,
Z)) →
quote(
X)
first1(
0',
Z) →
nil1first1(
s(
X),
cons(
Y,
Z)) →
cons1(
quote(
Y),
first1(
X,
activate(
Z)))
quote(
n__0) →
01'quote1(
n__cons(
X,
Z)) →
cons1(
quote(
activate(
X)),
quote1(
activate(
Z)))
quote1(
n__nil) →
nil1quote(
n__s(
X)) →
s1(
quote(
activate(
X)))
quote(
n__sel(
X,
Z)) →
sel1(
activate(
X),
activate(
Z))
quote1(
n__first(
X,
Z)) →
first1(
activate(
X),
activate(
Z))
unquote(
01') →
0'unquote(
s1(
X)) →
s(
unquote(
X))
unquote1(
nil1) →
nilunquote1(
cons1(
X,
Z)) →
fcons(
unquote(
X),
unquote1(
Z))
fcons(
X,
Z) →
cons(
X,
Z)
first(
X1,
X2) →
n__first(
X1,
X2)
from(
X) →
n__from(
X)
s(
X) →
n__s(
X)
0' →
n__0cons(
X1,
X2) →
n__cons(
X1,
X2)
nil →
n__nilsel(
X1,
X2) →
n__sel(
X1,
X2)
activate(
n__first(
X1,
X2)) →
first(
activate(
X1),
activate(
X2))
activate(
n__from(
X)) →
from(
activate(
X))
activate(
n__s(
X)) →
s(
activate(
X))
activate(
n__0) →
0'activate(
n__cons(
X1,
X2)) →
cons(
activate(
X1),
X2)
activate(
n__nil) →
nilactivate(
n__sel(
X1,
X2)) →
sel(
activate(
X1),
activate(
X2))
activate(
X) →
XTypes:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1
Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))
The following defined symbols remain to be analysed:
unquote, sel, activate, sel1, quote, first1, quote1, unquote1
They will be analysed ascendingly in the following order:
sel = activate
activate < sel1
activate < quote
activate < first1
activate < quote1
sel1 = quote
quote < first1
quote < quote1
first1 < quote1
unquote < unquote1
(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol unquote.
(10) Obligation:
TRS:
Rules:
sel(
s(
X),
cons(
Y,
Z)) →
sel(
X,
activate(
Z))
sel(
0',
cons(
X,
Z)) →
Xfirst(
0',
Z) →
nilfirst(
s(
X),
cons(
Y,
Z)) →
cons(
Y,
n__first(
X,
activate(
Z)))
from(
X) →
cons(
X,
n__from(
n__s(
X)))
sel1(
s(
X),
cons(
Y,
Z)) →
sel1(
X,
activate(
Z))
sel1(
0',
cons(
X,
Z)) →
quote(
X)
first1(
0',
Z) →
nil1first1(
s(
X),
cons(
Y,
Z)) →
cons1(
quote(
Y),
first1(
X,
activate(
Z)))
quote(
n__0) →
01'quote1(
n__cons(
X,
Z)) →
cons1(
quote(
activate(
X)),
quote1(
activate(
Z)))
quote1(
n__nil) →
nil1quote(
n__s(
X)) →
s1(
quote(
activate(
X)))
quote(
n__sel(
X,
Z)) →
sel1(
activate(
X),
activate(
Z))
quote1(
n__first(
X,
Z)) →
first1(
activate(
X),
activate(
Z))
unquote(
01') →
0'unquote(
s1(
X)) →
s(
unquote(
X))
unquote1(
nil1) →
nilunquote1(
cons1(
X,
Z)) →
fcons(
unquote(
X),
unquote1(
Z))
fcons(
X,
Z) →
cons(
X,
Z)
first(
X1,
X2) →
n__first(
X1,
X2)
from(
X) →
n__from(
X)
s(
X) →
n__s(
X)
0' →
n__0cons(
X1,
X2) →
n__cons(
X1,
X2)
nil →
n__nilsel(
X1,
X2) →
n__sel(
X1,
X2)
activate(
n__first(
X1,
X2)) →
first(
activate(
X1),
activate(
X2))
activate(
n__from(
X)) →
from(
activate(
X))
activate(
n__s(
X)) →
s(
activate(
X))
activate(
n__0) →
0'activate(
n__cons(
X1,
X2)) →
cons(
activate(
X1),
X2)
activate(
n__nil) →
nilactivate(
n__sel(
X1,
X2)) →
sel(
activate(
X1),
activate(
X2))
activate(
X) →
XTypes:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1
Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))
The following defined symbols remain to be analysed:
unquote1, sel, activate, sel1, quote, first1, quote1
They will be analysed ascendingly in the following order:
sel = activate
activate < sel1
activate < quote
activate < first1
activate < quote1
sel1 = quote
quote < first1
quote < quote1
first1 < quote1
(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol unquote1.
(12) Obligation:
TRS:
Rules:
sel(
s(
X),
cons(
Y,
Z)) →
sel(
X,
activate(
Z))
sel(
0',
cons(
X,
Z)) →
Xfirst(
0',
Z) →
nilfirst(
s(
X),
cons(
Y,
Z)) →
cons(
Y,
n__first(
X,
activate(
Z)))
from(
X) →
cons(
X,
n__from(
n__s(
X)))
sel1(
s(
X),
cons(
Y,
Z)) →
sel1(
X,
activate(
Z))
sel1(
0',
cons(
X,
Z)) →
quote(
X)
first1(
0',
Z) →
nil1first1(
s(
X),
cons(
Y,
Z)) →
cons1(
quote(
Y),
first1(
X,
activate(
Z)))
quote(
n__0) →
01'quote1(
n__cons(
X,
Z)) →
cons1(
quote(
activate(
X)),
quote1(
activate(
Z)))
quote1(
n__nil) →
nil1quote(
n__s(
X)) →
s1(
quote(
activate(
X)))
quote(
n__sel(
X,
Z)) →
sel1(
activate(
X),
activate(
Z))
quote1(
n__first(
X,
Z)) →
first1(
activate(
X),
activate(
Z))
unquote(
01') →
0'unquote(
s1(
X)) →
s(
unquote(
X))
unquote1(
nil1) →
nilunquote1(
cons1(
X,
Z)) →
fcons(
unquote(
X),
unquote1(
Z))
fcons(
X,
Z) →
cons(
X,
Z)
first(
X1,
X2) →
n__first(
X1,
X2)
from(
X) →
n__from(
X)
s(
X) →
n__s(
X)
0' →
n__0cons(
X1,
X2) →
n__cons(
X1,
X2)
nil →
n__nilsel(
X1,
X2) →
n__sel(
X1,
X2)
activate(
n__first(
X1,
X2)) →
first(
activate(
X1),
activate(
X2))
activate(
n__from(
X)) →
from(
activate(
X))
activate(
n__s(
X)) →
s(
activate(
X))
activate(
n__0) →
0'activate(
n__cons(
X1,
X2)) →
cons(
activate(
X1),
X2)
activate(
n__nil) →
nilactivate(
n__sel(
X1,
X2)) →
sel(
activate(
X1),
activate(
X2))
activate(
X) →
XTypes:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1
Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))
The following defined symbols remain to be analysed:
activate, sel, sel1, quote, first1, quote1
They will be analysed ascendingly in the following order:
sel = activate
activate < sel1
activate < quote
activate < first1
activate < quote1
sel1 = quote
quote < first1
quote < quote1
first1 < quote1
(13) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
activate(
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(
n5269_3)) →
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(
n5269_3), rt ∈ Ω(1 + n5269
3)
Induction Base:
activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0)) →RΩ(1)
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0)
Induction Step:
activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(n5269_3, 1))) →RΩ(1)
first(activate(n__0), activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n5269_3))) →RΩ(1)
first(n__0, activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n5269_3))) →IH
first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(c5270_3)) →RΩ(1)
n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n5269_3))
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(14) Complex Obligation (BEST)
(15) Obligation:
TRS:
Rules:
sel(
s(
X),
cons(
Y,
Z)) →
sel(
X,
activate(
Z))
sel(
0',
cons(
X,
Z)) →
Xfirst(
0',
Z) →
nilfirst(
s(
X),
cons(
Y,
Z)) →
cons(
Y,
n__first(
X,
activate(
Z)))
from(
X) →
cons(
X,
n__from(
n__s(
X)))
sel1(
s(
X),
cons(
Y,
Z)) →
sel1(
X,
activate(
Z))
sel1(
0',
cons(
X,
Z)) →
quote(
X)
first1(
0',
Z) →
nil1first1(
s(
X),
cons(
Y,
Z)) →
cons1(
quote(
Y),
first1(
X,
activate(
Z)))
quote(
n__0) →
01'quote1(
n__cons(
X,
Z)) →
cons1(
quote(
activate(
X)),
quote1(
activate(
Z)))
quote1(
n__nil) →
nil1quote(
n__s(
X)) →
s1(
quote(
activate(
X)))
quote(
n__sel(
X,
Z)) →
sel1(
activate(
X),
activate(
Z))
quote1(
n__first(
X,
Z)) →
first1(
activate(
X),
activate(
Z))
unquote(
01') →
0'unquote(
s1(
X)) →
s(
unquote(
X))
unquote1(
nil1) →
nilunquote1(
cons1(
X,
Z)) →
fcons(
unquote(
X),
unquote1(
Z))
fcons(
X,
Z) →
cons(
X,
Z)
first(
X1,
X2) →
n__first(
X1,
X2)
from(
X) →
n__from(
X)
s(
X) →
n__s(
X)
0' →
n__0cons(
X1,
X2) →
n__cons(
X1,
X2)
nil →
n__nilsel(
X1,
X2) →
n__sel(
X1,
X2)
activate(
n__first(
X1,
X2)) →
first(
activate(
X1),
activate(
X2))
activate(
n__from(
X)) →
from(
activate(
X))
activate(
n__s(
X)) →
s(
activate(
X))
activate(
n__0) →
0'activate(
n__cons(
X1,
X2)) →
cons(
activate(
X1),
X2)
activate(
n__nil) →
nilactivate(
n__sel(
X1,
X2)) →
sel(
activate(
X1),
activate(
X2))
activate(
X) →
XTypes:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1
Lemmas:
activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n5269_3)) → gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n5269_3), rt ∈ Ω(1 + n52693)
Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))
The following defined symbols remain to be analysed:
sel, sel1, quote, first1, quote1
They will be analysed ascendingly in the following order:
sel = activate
activate < sel1
activate < quote
activate < first1
activate < quote1
sel1 = quote
quote < first1
quote < quote1
first1 < quote1
(16) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol sel.
(17) Obligation:
TRS:
Rules:
sel(
s(
X),
cons(
Y,
Z)) →
sel(
X,
activate(
Z))
sel(
0',
cons(
X,
Z)) →
Xfirst(
0',
Z) →
nilfirst(
s(
X),
cons(
Y,
Z)) →
cons(
Y,
n__first(
X,
activate(
Z)))
from(
X) →
cons(
X,
n__from(
n__s(
X)))
sel1(
s(
X),
cons(
Y,
Z)) →
sel1(
X,
activate(
Z))
sel1(
0',
cons(
X,
Z)) →
quote(
X)
first1(
0',
Z) →
nil1first1(
s(
X),
cons(
Y,
Z)) →
cons1(
quote(
Y),
first1(
X,
activate(
Z)))
quote(
n__0) →
01'quote1(
n__cons(
X,
Z)) →
cons1(
quote(
activate(
X)),
quote1(
activate(
Z)))
quote1(
n__nil) →
nil1quote(
n__s(
X)) →
s1(
quote(
activate(
X)))
quote(
n__sel(
X,
Z)) →
sel1(
activate(
X),
activate(
Z))
quote1(
n__first(
X,
Z)) →
first1(
activate(
X),
activate(
Z))
unquote(
01') →
0'unquote(
s1(
X)) →
s(
unquote(
X))
unquote1(
nil1) →
nilunquote1(
cons1(
X,
Z)) →
fcons(
unquote(
X),
unquote1(
Z))
fcons(
X,
Z) →
cons(
X,
Z)
first(
X1,
X2) →
n__first(
X1,
X2)
from(
X) →
n__from(
X)
s(
X) →
n__s(
X)
0' →
n__0cons(
X1,
X2) →
n__cons(
X1,
X2)
nil →
n__nilsel(
X1,
X2) →
n__sel(
X1,
X2)
activate(
n__first(
X1,
X2)) →
first(
activate(
X1),
activate(
X2))
activate(
n__from(
X)) →
from(
activate(
X))
activate(
n__s(
X)) →
s(
activate(
X))
activate(
n__0) →
0'activate(
n__cons(
X1,
X2)) →
cons(
activate(
X1),
X2)
activate(
n__nil) →
nilactivate(
n__sel(
X1,
X2)) →
sel(
activate(
X1),
activate(
X2))
activate(
X) →
XTypes:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1
Lemmas:
activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n5269_3)) → gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n5269_3), rt ∈ Ω(1 + n52693)
Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))
The following defined symbols remain to be analysed:
quote, sel1, first1, quote1
They will be analysed ascendingly in the following order:
sel1 = quote
quote < first1
quote < quote1
first1 < quote1
(18) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol quote.
(19) Obligation:
TRS:
Rules:
sel(
s(
X),
cons(
Y,
Z)) →
sel(
X,
activate(
Z))
sel(
0',
cons(
X,
Z)) →
Xfirst(
0',
Z) →
nilfirst(
s(
X),
cons(
Y,
Z)) →
cons(
Y,
n__first(
X,
activate(
Z)))
from(
X) →
cons(
X,
n__from(
n__s(
X)))
sel1(
s(
X),
cons(
Y,
Z)) →
sel1(
X,
activate(
Z))
sel1(
0',
cons(
X,
Z)) →
quote(
X)
first1(
0',
Z) →
nil1first1(
s(
X),
cons(
Y,
Z)) →
cons1(
quote(
Y),
first1(
X,
activate(
Z)))
quote(
n__0) →
01'quote1(
n__cons(
X,
Z)) →
cons1(
quote(
activate(
X)),
quote1(
activate(
Z)))
quote1(
n__nil) →
nil1quote(
n__s(
X)) →
s1(
quote(
activate(
X)))
quote(
n__sel(
X,
Z)) →
sel1(
activate(
X),
activate(
Z))
quote1(
n__first(
X,
Z)) →
first1(
activate(
X),
activate(
Z))
unquote(
01') →
0'unquote(
s1(
X)) →
s(
unquote(
X))
unquote1(
nil1) →
nilunquote1(
cons1(
X,
Z)) →
fcons(
unquote(
X),
unquote1(
Z))
fcons(
X,
Z) →
cons(
X,
Z)
first(
X1,
X2) →
n__first(
X1,
X2)
from(
X) →
n__from(
X)
s(
X) →
n__s(
X)
0' →
n__0cons(
X1,
X2) →
n__cons(
X1,
X2)
nil →
n__nilsel(
X1,
X2) →
n__sel(
X1,
X2)
activate(
n__first(
X1,
X2)) →
first(
activate(
X1),
activate(
X2))
activate(
n__from(
X)) →
from(
activate(
X))
activate(
n__s(
X)) →
s(
activate(
X))
activate(
n__0) →
0'activate(
n__cons(
X1,
X2)) →
cons(
activate(
X1),
X2)
activate(
n__nil) →
nilactivate(
n__sel(
X1,
X2)) →
sel(
activate(
X1),
activate(
X2))
activate(
X) →
XTypes:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1
Lemmas:
activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n5269_3)) → gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n5269_3), rt ∈ Ω(1 + n52693)
Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))
The following defined symbols remain to be analysed:
sel1, first1, quote1
They will be analysed ascendingly in the following order:
sel1 = quote
quote < first1
quote < quote1
first1 < quote1
(20) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol sel1.
(21) Obligation:
TRS:
Rules:
sel(
s(
X),
cons(
Y,
Z)) →
sel(
X,
activate(
Z))
sel(
0',
cons(
X,
Z)) →
Xfirst(
0',
Z) →
nilfirst(
s(
X),
cons(
Y,
Z)) →
cons(
Y,
n__first(
X,
activate(
Z)))
from(
X) →
cons(
X,
n__from(
n__s(
X)))
sel1(
s(
X),
cons(
Y,
Z)) →
sel1(
X,
activate(
Z))
sel1(
0',
cons(
X,
Z)) →
quote(
X)
first1(
0',
Z) →
nil1first1(
s(
X),
cons(
Y,
Z)) →
cons1(
quote(
Y),
first1(
X,
activate(
Z)))
quote(
n__0) →
01'quote1(
n__cons(
X,
Z)) →
cons1(
quote(
activate(
X)),
quote1(
activate(
Z)))
quote1(
n__nil) →
nil1quote(
n__s(
X)) →
s1(
quote(
activate(
X)))
quote(
n__sel(
X,
Z)) →
sel1(
activate(
X),
activate(
Z))
quote1(
n__first(
X,
Z)) →
first1(
activate(
X),
activate(
Z))
unquote(
01') →
0'unquote(
s1(
X)) →
s(
unquote(
X))
unquote1(
nil1) →
nilunquote1(
cons1(
X,
Z)) →
fcons(
unquote(
X),
unquote1(
Z))
fcons(
X,
Z) →
cons(
X,
Z)
first(
X1,
X2) →
n__first(
X1,
X2)
from(
X) →
n__from(
X)
s(
X) →
n__s(
X)
0' →
n__0cons(
X1,
X2) →
n__cons(
X1,
X2)
nil →
n__nilsel(
X1,
X2) →
n__sel(
X1,
X2)
activate(
n__first(
X1,
X2)) →
first(
activate(
X1),
activate(
X2))
activate(
n__from(
X)) →
from(
activate(
X))
activate(
n__s(
X)) →
s(
activate(
X))
activate(
n__0) →
0'activate(
n__cons(
X1,
X2)) →
cons(
activate(
X1),
X2)
activate(
n__nil) →
nilactivate(
n__sel(
X1,
X2)) →
sel(
activate(
X1),
activate(
X2))
activate(
X) →
XTypes:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1
Lemmas:
activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n5269_3)) → gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n5269_3), rt ∈ Ω(1 + n52693)
Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))
The following defined symbols remain to be analysed:
first1, quote1
They will be analysed ascendingly in the following order:
first1 < quote1
(22) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol first1.
(23) Obligation:
TRS:
Rules:
sel(
s(
X),
cons(
Y,
Z)) →
sel(
X,
activate(
Z))
sel(
0',
cons(
X,
Z)) →
Xfirst(
0',
Z) →
nilfirst(
s(
X),
cons(
Y,
Z)) →
cons(
Y,
n__first(
X,
activate(
Z)))
from(
X) →
cons(
X,
n__from(
n__s(
X)))
sel1(
s(
X),
cons(
Y,
Z)) →
sel1(
X,
activate(
Z))
sel1(
0',
cons(
X,
Z)) →
quote(
X)
first1(
0',
Z) →
nil1first1(
s(
X),
cons(
Y,
Z)) →
cons1(
quote(
Y),
first1(
X,
activate(
Z)))
quote(
n__0) →
01'quote1(
n__cons(
X,
Z)) →
cons1(
quote(
activate(
X)),
quote1(
activate(
Z)))
quote1(
n__nil) →
nil1quote(
n__s(
X)) →
s1(
quote(
activate(
X)))
quote(
n__sel(
X,
Z)) →
sel1(
activate(
X),
activate(
Z))
quote1(
n__first(
X,
Z)) →
first1(
activate(
X),
activate(
Z))
unquote(
01') →
0'unquote(
s1(
X)) →
s(
unquote(
X))
unquote1(
nil1) →
nilunquote1(
cons1(
X,
Z)) →
fcons(
unquote(
X),
unquote1(
Z))
fcons(
X,
Z) →
cons(
X,
Z)
first(
X1,
X2) →
n__first(
X1,
X2)
from(
X) →
n__from(
X)
s(
X) →
n__s(
X)
0' →
n__0cons(
X1,
X2) →
n__cons(
X1,
X2)
nil →
n__nilsel(
X1,
X2) →
n__sel(
X1,
X2)
activate(
n__first(
X1,
X2)) →
first(
activate(
X1),
activate(
X2))
activate(
n__from(
X)) →
from(
activate(
X))
activate(
n__s(
X)) →
s(
activate(
X))
activate(
n__0) →
0'activate(
n__cons(
X1,
X2)) →
cons(
activate(
X1),
X2)
activate(
n__nil) →
nilactivate(
n__sel(
X1,
X2)) →
sel(
activate(
X1),
activate(
X2))
activate(
X) →
XTypes:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1
Lemmas:
activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n5269_3)) → gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n5269_3), rt ∈ Ω(1 + n52693)
Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))
The following defined symbols remain to be analysed:
quote1
(24) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol quote1.
(25) Obligation:
TRS:
Rules:
sel(
s(
X),
cons(
Y,
Z)) →
sel(
X,
activate(
Z))
sel(
0',
cons(
X,
Z)) →
Xfirst(
0',
Z) →
nilfirst(
s(
X),
cons(
Y,
Z)) →
cons(
Y,
n__first(
X,
activate(
Z)))
from(
X) →
cons(
X,
n__from(
n__s(
X)))
sel1(
s(
X),
cons(
Y,
Z)) →
sel1(
X,
activate(
Z))
sel1(
0',
cons(
X,
Z)) →
quote(
X)
first1(
0',
Z) →
nil1first1(
s(
X),
cons(
Y,
Z)) →
cons1(
quote(
Y),
first1(
X,
activate(
Z)))
quote(
n__0) →
01'quote1(
n__cons(
X,
Z)) →
cons1(
quote(
activate(
X)),
quote1(
activate(
Z)))
quote1(
n__nil) →
nil1quote(
n__s(
X)) →
s1(
quote(
activate(
X)))
quote(
n__sel(
X,
Z)) →
sel1(
activate(
X),
activate(
Z))
quote1(
n__first(
X,
Z)) →
first1(
activate(
X),
activate(
Z))
unquote(
01') →
0'unquote(
s1(
X)) →
s(
unquote(
X))
unquote1(
nil1) →
nilunquote1(
cons1(
X,
Z)) →
fcons(
unquote(
X),
unquote1(
Z))
fcons(
X,
Z) →
cons(
X,
Z)
first(
X1,
X2) →
n__first(
X1,
X2)
from(
X) →
n__from(
X)
s(
X) →
n__s(
X)
0' →
n__0cons(
X1,
X2) →
n__cons(
X1,
X2)
nil →
n__nilsel(
X1,
X2) →
n__sel(
X1,
X2)
activate(
n__first(
X1,
X2)) →
first(
activate(
X1),
activate(
X2))
activate(
n__from(
X)) →
from(
activate(
X))
activate(
n__s(
X)) →
s(
activate(
X))
activate(
n__0) →
0'activate(
n__cons(
X1,
X2)) →
cons(
activate(
X1),
X2)
activate(
n__nil) →
nilactivate(
n__sel(
X1,
X2)) →
sel(
activate(
X1),
activate(
X2))
activate(
X) →
XTypes:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1
Lemmas:
activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n5269_3)) → gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n5269_3), rt ∈ Ω(1 + n52693)
Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))
No more defined symbols left to analyse.
(26) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n5269_3)) → gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n5269_3), rt ∈ Ω(1 + n52693)
(27) BOUNDS(n^1, INF)
(28) Obligation:
TRS:
Rules:
sel(
s(
X),
cons(
Y,
Z)) →
sel(
X,
activate(
Z))
sel(
0',
cons(
X,
Z)) →
Xfirst(
0',
Z) →
nilfirst(
s(
X),
cons(
Y,
Z)) →
cons(
Y,
n__first(
X,
activate(
Z)))
from(
X) →
cons(
X,
n__from(
n__s(
X)))
sel1(
s(
X),
cons(
Y,
Z)) →
sel1(
X,
activate(
Z))
sel1(
0',
cons(
X,
Z)) →
quote(
X)
first1(
0',
Z) →
nil1first1(
s(
X),
cons(
Y,
Z)) →
cons1(
quote(
Y),
first1(
X,
activate(
Z)))
quote(
n__0) →
01'quote1(
n__cons(
X,
Z)) →
cons1(
quote(
activate(
X)),
quote1(
activate(
Z)))
quote1(
n__nil) →
nil1quote(
n__s(
X)) →
s1(
quote(
activate(
X)))
quote(
n__sel(
X,
Z)) →
sel1(
activate(
X),
activate(
Z))
quote1(
n__first(
X,
Z)) →
first1(
activate(
X),
activate(
Z))
unquote(
01') →
0'unquote(
s1(
X)) →
s(
unquote(
X))
unquote1(
nil1) →
nilunquote1(
cons1(
X,
Z)) →
fcons(
unquote(
X),
unquote1(
Z))
fcons(
X,
Z) →
cons(
X,
Z)
first(
X1,
X2) →
n__first(
X1,
X2)
from(
X) →
n__from(
X)
s(
X) →
n__s(
X)
0' →
n__0cons(
X1,
X2) →
n__cons(
X1,
X2)
nil →
n__nilsel(
X1,
X2) →
n__sel(
X1,
X2)
activate(
n__first(
X1,
X2)) →
first(
activate(
X1),
activate(
X2))
activate(
n__from(
X)) →
from(
activate(
X))
activate(
n__s(
X)) →
s(
activate(
X))
activate(
n__0) →
0'activate(
n__cons(
X1,
X2)) →
cons(
activate(
X1),
X2)
activate(
n__nil) →
nilactivate(
n__sel(
X1,
X2)) →
sel(
activate(
X1),
activate(
X2))
activate(
X) →
XTypes:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1
Lemmas:
activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n5269_3)) → gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n5269_3), rt ∈ Ω(1 + n52693)
Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))
No more defined symbols left to analyse.
(29) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n5269_3)) → gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n5269_3), rt ∈ Ω(1 + n52693)
(30) BOUNDS(n^1, INF)